Hoare logic
ホーア論理
Assertion
(software development)
Denotational semantics
Design by contract
Dynamic logic
Formal verification
Loop invariant
Predicate transformer semantics
Static program analysis
https://en.wikipedia.org/wiki/Hoare_logic